w-atom-constraint(w)
== (i, x:Id. AtomFree(Type;w.T(i,x)))
== & (i, a:Id. AtomFree(Type;w.TA(i,a)))
== & (l:IdLnk, tg:Id. AtomFree(Type;w.M(l,tg))) 

latex

---

clarification:

w-atom-constraint{i:l}
w-atom-constraint(w)
== (i:Id, x:Id. AtomFree(Type{i};w.T(i,x)))
== & (i:Id, a:Id. AtomFree(Type{i};w.TA(i,a)))
== & (l:IdLnk, tg:Id. AtomFree(Type{i};w.M(l,tg))) 

latex

Definitions	w.T, P & Q, w.TA, IdLnk, x:A. B(x), Id, AtomFree(T;x), Type, f(a), w.M
FDL editor aliases	w-atom-constraint